(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun ae () Real)
(declare-fun af () Real)
(assert (forall ((m Real)) (= f (/ m o))))
(assert (or (and (and (and (or (or (and (or (or (or (and (and (and (xor (< 0.0 (* ab i) (/ 7 b k)) (and (and (< 0.0 (/ 77 (+ (* c ac) (- 2 ab)) aa)) (> (/ 7 aa) f)) (<= i (/ 2 e f)))) (<= 0.0 (* b k))) (distinct j 1.0)) (< (- (/ 6 (- 10 a q) (* (+ 6 aa) (- 2.0 ad))) (/ (- 215 (- 216 (+ c ac))) (+ 30 (+ (- (* c ac) (/ 10 203)) (/ f (- 51 e f))) (* 131 (* 33 e f) aa)))) l)) (<= 0.0 aa)) (<= aa af)) (>= (* (+ a q) (- 9 ad)) l)) (= n 2.0)) (>= 0 l)) (>= 0.0 ad)) (< 0.0 ae) (<= ae af c ac)) (> 0.0 af)) (> 0.0 (+ e f))) (>= 0.0 (* (/ 82 (* 2 c ac) (+ 7 b k)) aa) (/ 91 aa))))
(assert (distinct d h))
(assert (distinct g p))
(check-sat)
